Calculus of Inductive Constructions(CIC)

#Fleeting_Notes

Calculus of Constructions(CoC) + 帰納型(Inductive Type)が使えるもの

単純型付きラムダ計算 + 依存型 + 型構築子 + ポリモーフィズム(多相型) + 帰納型

CoCはラムダ・キューブではλC

CICを基に構築されているもの

Coq

Lean

確認用

Q. Calculus of Inductive Constructions(CIC)

関連

『Sets in Coq, Coq in Sets』

Bruno Barras. Sets in Coq, Coq in Sets. Journal of Formalized Reasoning, 3(1):29–48, 2010. 4

『On the Role of Type Decorations in the Calculus of Inductive Constructions』

Bruno Barras and Benjamin Gr ́egoire. On the Role of Type Decorations in the Calculus of Inductive Constructions. In International Workshop on Computer Science Logic, pages 151166. Springer, 2005.

『Coq in Coq』

Bruno Barras and Benjamin Werner. Coq in Coq. Available on the WWW, 1997.

調査用

Google.icon Calculus of Inductive Constructions(CIC)(日)

Google.icon Calculus of inductive constructions(CIC)(英)

Wikipedia.icon

Calculus of Inductive Constructions - Wikipedia(日)

Calculus of Inductive Constructions(検索) - Wikipedia(日)

Wikipedia.icon

Calculus of inductive constructions - Wikipedia(英)

Calculus of inductive constructions(検索) - Wikipedia(英)